es:ES, T:Type, I:MaInterface(T).
ma-interface-consistent(es;I)  ([[I|]]  (AbsInterface(T) List)) 

latex

Definitions	[[I|]], t  T, AbsInterface(A), type List, ma-interface-consistent(es;X), P  Q, MaInterface(T), x:A. B(x), Type, ES, Id, (x  l), {x:A| B(x)} , x:AB(x), [[I|i]], x.A(x), ma-interface-locs(I), IdDeq, remove-repeats(eq;L), False, A, left + right, P  Q, Dec(P), x:A  B(x), b, a:A fp B(a), ma-interface-consistent-at(es;i;X), Atom$n, s = t, P & Q, P  Q
Lemmas	member-remove-repeats, decidable l member, decidable equal Id, map-wf2, Id wf, es-interface wf, remove-repeats wf, id-deq wf, ma-interface-locs wf, ma-interface-triggers wf, l member wf